$\forall$$p$:FinProbSpace, $f$:($\mathbb{N}\rightarrow\mathbb{N}$), $X$:($n$:$\mathbb{N}\rightarrow$RandomVariable($p$;$f$($n$))).
\\[0ex]($\forall$$n$:$\mathbb{N}$, $i$:\{0..$n$$^{-}$\}. $f$($i$) $<$ $f$($n$))
\\[0ex]$\Rightarrow$ ($\forall$$n$:$\mathbb{N}$. 0 $\leq$ $X$($n$))
\\[0ex]$\Rightarrow$ ($\forall$$m$:$\mathbb{N}$, $n$:\{0..($m$+1)$^{-}$\}. rv{-}partial{-}sum($n$;$i$.$X$($i$)) $\leq$ rv{-}partial{-}sum($m$;$i$.$X$($i$)))